00100	GIVEAX(TERM1,(∀ X)(ISVAR X ⊃ ISTERM X));
00200	
00300	GIVEAX(TERM2,(∀ X)(ISVAR X ⊃ ISSET DOM X));
00400	
00500	GIVEAX(TERM3,(∀ X)(ISCONST X ⊃ ISTERM X));
00600	
00700	GIVEAX(TERM4,(∀ X)(ISCONST X ⊃ ISSET DOM X));
00800	
00900	GIVEAX(TERM5,(∀ X)(ISCONST X ⊃ VALUE X ε DOM X));
01000	
01100	GIVEAX(TERM6,(∀ X)(∀ U)(ISVAR X ∧ ISASSIGN U ⊃ VAL(X,U) ε
01200		DOM X));
01300	
01400	GIVEAX(TERM7,(∀ X)(∀ W)(XεW ⊃ ISCONST MKCONST(X,W)
01500		∧ DOM MKCONST(X,W)=W ∧ VALUE MKCONST(X,W) = X));
01600	
01700	GIVEAX(TERM10,(∀ X)(ISVAR X ⊃ VARS X = UNITSET X));
01800	
01900	GIVEAX(TERM11,(∀ X)(ISCONST X ≡ VARS X = NULSET));
02000	
02100	GIVEAX(TERM12,(∀ X)(∀ U)(ISCONST X ∧ ISASSIGN U ⊃ VAL(X,U)=VALUE X));
02200	
02300	GIVEAX(TERM13,(∀ F)(∀ X)(∀ U)(∀ V)(ISTERM F ∧ ISTERM X 
02400		∧ DOM F = (U→V) ∧ DOM X = U ⊃
02500		ISTERM α(F,X) ∧
02600		DOM α(F,X) = V ∧
02700		VARS α(F,X) = VARS F ∪ VARS X ∧
02800		(∀ U)(ISASSIGN U ⊃
02900			VAL(α(F,X),U) = β(VAL(F,U),VAL(X,U)))));
03000	
03100	GIVEAX(TERM14,(∀ X)(∀ Y)(ISVAR X ∧ ISTERM Y ⊃
03200		ISTERM LL(X,Y) ∧
03300		DOM LL(X,Y) = (DOM X → DOM Y) ∧
03400		VARS LL(X,Y) = SETDIFF(VARS Y,VARS X) ∧
03500		(∀ U)(∀ W)(ISASSIGN U ∧ W ε DOM X ⊃
03600			β(VAL(LL(X,Y),U),W) = VAL(Y,A(X,W,U)))));
03700	
03800	GIVEAX(TERM15,(∀ X)(∀ W)(∀ U)(ISVAR X ∧ W ε DOM X ∧
03900			ISASSIGN U ⊃
04000		ISASSIGN A(X,W,U) ∧
04100		VAL(X,A(X,W,U)) = W ∧
04200		(∀ Y)(ISVAR Y ∧ Y≠X ⊃ VAL(Y,A(X,W,U)) = VAL(Y,U))));
     

00100	END;